(DEFPROP SETUP 
 (LAMBDA(Z)
  (PROG (BL Z1 Z2 Z3 Z4 Z5 M)
   SET2 (SETQ Z3 (CAR Z))
	(SETQ Z2 0)
	(SETQ BL NIL)
	(SETQ NO* NO)
	(SETQ Z5 NIL)
   S1   (SETQ Z4 (MIN1 Z3))
	(COND ((NULL Z4) (GO S3)))
	(UPIT Z4)
	(SETQ Z2 (ADD1 Z2))
	(SETQ M (UN Z4 M))
	(SETQ Z5 (CONS Z4 Z5))
	(GO S1)
   S3   (SETQ Z3 NIL)
	(SETQ Z4 Z5)
   S2   (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
	(SETQ Z4 (CDR Z4))
	(COND (Z4 (GO S2)))
   SET3 (SETQ Z5 (CONS (LIST Z2 Z3 AXNO AXNO) Z5))
   SET1 (SETQ Z1 (CONS Z5 Z1))
	(SETQ Z (CDR Z))
	(SETQ AXNO (ADD1 AXNO))
	(COND (Z (GO SET2)))
	(RETURN (CONS Z1 M)))) 
EXPR)

(DEFPROP BOOKEEP 
 (LAMBDA(L M N)
  (PROG (U C)
	(COND ((ALLPOS (CAR N)) NIL) (T (SETQ N (CONS (CDR N) (CAR N)))))
   B1   (SETQ C CNT)
	(SETQ U M)
   B3   (RPLACD (CDAAR U) (CONS C N))
	(SETQ U (CDR U))
	(COND ((NULL U) (RETURN (NCONC L M))))
	(SETQ C (ADD1 C))
	(GO B3))) 
EXPR)

(DEFPROP TRYPRF 
 (LAMBDA(U)
  (PROG (Z1 Z2 R)
   TRY4 TRY3
	(SETQ XX (CHOICE XX EE EE1))
	(COND ((NULL XX) (GO TRY7)) ((EQ XX T) (GO TRY7)))
	(SETQ Z1 (CAAR XX))
	(SETQ Z2 (CADR XX))
	(COND ((OR (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY6F)))
   TRY2 TRY1
	(COND ((NOT STRATEGY) (GO TRY1A)))
	(COND ((OR (STRATEGY Z1) (STRATEGY Z2)) (GO TRY1A)) (T (GO TRY6F)))
   TRY1A
	(COND ((NOT (SINGCON Z1 Z2)) (GO TRY6F)))
	(COND ((AND (ALLPOS Z1) (ALLPOS Z2)) (GO TRY6)) ((AND (ALLNEG Z1) (ALLNEG Z2)) (GO TRY8)))
	(SETQ R (RESOLVE Z1 Z2))
   TRY10
	(COND ((NULL R) (GO TRY6A)) ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
	(SETQ CNT (PLUS CNT (FINI U R Z1 Z2 EE1)))
   TRY6A
   TRY6 (COND ((OR PFLG (NOT (HERE Z1)) (NOT (HERE Z2))) (GO TRY6F)))
	(SETQ R (PARMOD Z1 Z2))
	(COND ((NULL R) (GO TRY6F)))
	(SETQ CNT (PLUS CNT (FINI U R Z1 Z2 EE1)))
   TRY6F
   TRY6G
   TRY8 (COND ((TTYIN) (UPDATE CLAUSES)))
	(GO TRY3)
   TRY7 (PRINT (QUOTE COUNT))
	(PRINT COUNT)
	(PRINT (QUOTE LEVEL))
	(PRINT LVL)
	(SETQ LVL (ADD1 LVL))
	(PRINT (QUOTE ELAPSED-TIME))
	(PRINT (TIMEIT))
	(SETQ EE EE1)
	(SETQ XX (CONS U EE))
	(COND ((CDR EE) (SETQ EE1 (LAST EE)) (GO TRY4)))
	(PRINT (QUOTE NO-PROOF-FOUND))
	(COND (AUTO (ERR (QUOTE NOPROOF))))
	(UPDATE CLAUSES)
	(ERR (QUOTE NOPROOF))
   TRY6H)) 
EXPR)

(DEFPROP SINGCON 
 (LAMBDA(X Y)
  (PROG (Z)
	(COND ((ALLPOS Y) (SETQ Z Y) (SETQ Y X) (SETQ X Z)))
	(SETQ Z (ANCESTOR Y))
	(COND ((NULL (CDR Z)) (RETURN T))
	      (T (RETURN (NOT (GREATERP (CAR (MKWRD (CAR Z))) (CAR (MKWRD X))))))))) 
EXPR)